0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 1177 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 71 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 394 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 19 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 0 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
↳30 PiDP
↳31 UsableRulesProof (⇔, 0 ms)
↳32 PiDP
↳33 PiDPToQDPProof (⇒, 0 ms)
↳34 QDP
↳35 QDPSizeChangeProof (⇔, 0 ms)
↳36 YES
↳37 PiDP
↳38 UsableRulesProof (⇔, 0 ms)
↳39 PiDP
↳40 PiDPToQDPProof (⇒, 0 ms)
↳41 QDP
↳42 QDPSizeChangeProof (⇔, 0 ms)
↳43 YES
↳44 PiDP
↳45 UsableRulesProof (⇔, 0 ms)
↳46 PiDP
↳47 PiDPToQDPProof (⇒, 0 ms)
↳48 QDP
↳49 QDPSizeChangeProof (⇔, 0 ms)
↳50 YES
↳51 PiDP
↳52 UsableRulesProof (⇔, 0 ms)
↳53 PiDP
↳54 PiDPToQDPProof (⇒, 0 ms)
↳55 QDP
↳56 QDPSizeChangeProof (⇔, 0 ms)
↳57 YES
↳58 PiDP
↳59 UsableRulesProof (⇔, 0 ms)
↳60 PiDP
↳61 PiDPToQDPProof (⇒, 0 ms)
↳62 QDP
↳63 QDPSizeChangeProof (⇔, 0 ms)
↳64 YES
divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotA_in_ggga(0, s(T208), T209, 0) → quotA_out_ggga(0, s(T208), T209, 0)
quotA_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
quotA_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quotC_in_ga(T251, T253))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(0))), 0) → quotC_out_ga(s(s(s(0))), 0)
quotC_in_ga(s(s(s(s(0)))), 0) → quotC_out_ga(s(s(s(s(0)))), 0)
quotC_in_ga(s(s(s(s(s(0))))), 0) → quotC_out_ga(s(s(s(s(s(0))))), 0)
quotC_in_ga(s(s(s(s(s(s(0)))))), 0) → quotC_out_ga(s(s(s(s(s(s(0)))))), 0)
quotC_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_ga(T336, T338, quotC_in_ga(T336, T338))
U11_ga(T336, T338, quotC_out_ga(T336, T338)) → quotC_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U4_gga(T251, T253, quotC_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_gga(T350, T352, quotD_in_ga(T350, T352))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U12_ga(T424, T426, quotD_in_ga(T424, T426))
U12_ga(T424, T426, quotD_out_ga(T424, T426)) → quotD_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U5_gga(T350, T352, quotD_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_gga(T437, T439, quotE_in_ga(T437, T439))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T500))))), s(T502)) → U13_ga(T500, T502, quotE_in_ga(T500, T502))
U13_ga(T500, T502, quotE_out_ga(T500, T502)) → quotE_out_ga(s(s(s(s(s(T500))))), s(T502))
U6_gga(T437, T439, quotE_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_gga(T512, T514, quotF_in_ga(T512, T514))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(T564)))), s(T566)) → U14_ga(T564, T566, quotF_in_ga(T564, T566))
U14_ga(T564, T566, quotF_out_ga(T564, T566)) → quotF_out_ga(s(s(s(s(T564)))), s(T566))
U7_gga(T512, T514, quotF_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_gga(T575, T577, quotG_in_ga(T575, T577))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(T616))), s(T618)) → U15_ga(T616, T618, quotG_in_ga(T616, T618))
U15_ga(T616, T618, quotG_out_ga(T616, T618)) → quotG_out_ga(s(s(s(T616))), s(T618))
U8_gga(T575, T577, quotG_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U9_gga(T626, T628, quotH_in_ga(T626, T628))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(T656)), s(T658)) → U16_ga(T656, T658, quotH_in_ga(T656, T658))
U16_ga(T656, T658, quotH_out_ga(T656, T658)) → quotH_out_ga(s(s(T656)), s(T658))
U9_gga(T626, T628, quotH_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U10_gga(T665, T667, quotI_in_ga(T665, T667))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(T684), s(T686)) → U17_ga(T684, T686, quotI_in_ga(T684, T686))
U17_ga(T684, T686, quotI_out_ga(T684, T686)) → quotI_out_ga(s(T684), s(T686))
U10_gga(T665, T667, quotI_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U2_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotA_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quotA_out_ggga(T226, T227, T228, T230)) → quotA_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quotA_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotA_in_ggga(0, s(T208), T209, 0) → quotA_out_ggga(0, s(T208), T209, 0)
quotA_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
quotA_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quotC_in_ga(T251, T253))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(0))), 0) → quotC_out_ga(s(s(s(0))), 0)
quotC_in_ga(s(s(s(s(0)))), 0) → quotC_out_ga(s(s(s(s(0)))), 0)
quotC_in_ga(s(s(s(s(s(0))))), 0) → quotC_out_ga(s(s(s(s(s(0))))), 0)
quotC_in_ga(s(s(s(s(s(s(0)))))), 0) → quotC_out_ga(s(s(s(s(s(s(0)))))), 0)
quotC_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_ga(T336, T338, quotC_in_ga(T336, T338))
U11_ga(T336, T338, quotC_out_ga(T336, T338)) → quotC_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U4_gga(T251, T253, quotC_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_gga(T350, T352, quotD_in_ga(T350, T352))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U12_ga(T424, T426, quotD_in_ga(T424, T426))
U12_ga(T424, T426, quotD_out_ga(T424, T426)) → quotD_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U5_gga(T350, T352, quotD_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_gga(T437, T439, quotE_in_ga(T437, T439))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T500))))), s(T502)) → U13_ga(T500, T502, quotE_in_ga(T500, T502))
U13_ga(T500, T502, quotE_out_ga(T500, T502)) → quotE_out_ga(s(s(s(s(s(T500))))), s(T502))
U6_gga(T437, T439, quotE_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_gga(T512, T514, quotF_in_ga(T512, T514))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(T564)))), s(T566)) → U14_ga(T564, T566, quotF_in_ga(T564, T566))
U14_ga(T564, T566, quotF_out_ga(T564, T566)) → quotF_out_ga(s(s(s(s(T564)))), s(T566))
U7_gga(T512, T514, quotF_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_gga(T575, T577, quotG_in_ga(T575, T577))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(T616))), s(T618)) → U15_ga(T616, T618, quotG_in_ga(T616, T618))
U15_ga(T616, T618, quotG_out_ga(T616, T618)) → quotG_out_ga(s(s(s(T616))), s(T618))
U8_gga(T575, T577, quotG_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U9_gga(T626, T628, quotH_in_ga(T626, T628))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(T656)), s(T658)) → U16_ga(T656, T658, quotH_in_ga(T656, T658))
U16_ga(T656, T658, quotH_out_ga(T656, T658)) → quotH_out_ga(s(s(T656)), s(T658))
U9_gga(T626, T628, quotH_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U10_gga(T665, T667, quotI_in_ga(T665, T667))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(T684), s(T686)) → U17_ga(T684, T686, quotI_in_ga(T684, T686))
U17_ga(T684, T686, quotI_out_ga(T684, T686)) → quotI_out_ga(s(T684), s(T686))
U10_gga(T665, T667, quotI_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U2_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotA_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quotA_out_ggga(T226, T227, T228, T230)) → quotA_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quotA_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)
DIVJ_IN_GGA(T7, T8, T10) → U18_GGA(T7, T8, T10, quotB_in_gga(T7, T8, T10))
DIVJ_IN_GGA(T7, T8, T10) → QUOTB_IN_GGA(T7, T8, T10)
QUOTB_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_GGA(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
QUOTB_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → QUOTA_IN_GGGA(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)
QUOTA_IN_GGGA(s(T226), s(T227), T228, T230) → U1_GGGA(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
QUOTA_IN_GGGA(s(T226), s(T227), T228, T230) → QUOTA_IN_GGGA(T226, T227, T228, T230)
QUOTA_IN_GGGA(T241, 0, T242, s(T244)) → U2_GGGA(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
QUOTA_IN_GGGA(T241, 0, T242, s(T244)) → QUOTB_IN_GGA(T241, s(T242), T244)
QUOTB_IN_GGA(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_GGA(T251, T253, quotC_in_ga(T251, T253))
QUOTB_IN_GGA(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → QUOTC_IN_GA(T251, T253)
QUOTC_IN_GA(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_GA(T336, T338, quotC_in_ga(T336, T338))
QUOTC_IN_GA(s(s(s(s(s(s(s(T336))))))), s(T338)) → QUOTC_IN_GA(T336, T338)
QUOTB_IN_GGA(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_GGA(T350, T352, quotD_in_ga(T350, T352))
QUOTB_IN_GGA(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → QUOTD_IN_GA(T350, T352)
QUOTD_IN_GA(s(s(s(s(s(s(T424)))))), s(T426)) → U12_GA(T424, T426, quotD_in_ga(T424, T426))
QUOTD_IN_GA(s(s(s(s(s(s(T424)))))), s(T426)) → QUOTD_IN_GA(T424, T426)
QUOTB_IN_GGA(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_GGA(T437, T439, quotE_in_ga(T437, T439))
QUOTB_IN_GGA(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → QUOTE_IN_GA(T437, T439)
QUOTE_IN_GA(s(s(s(s(s(T500))))), s(T502)) → U13_GA(T500, T502, quotE_in_ga(T500, T502))
QUOTE_IN_GA(s(s(s(s(s(T500))))), s(T502)) → QUOTE_IN_GA(T500, T502)
QUOTB_IN_GGA(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_GGA(T512, T514, quotF_in_ga(T512, T514))
QUOTB_IN_GGA(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → QUOTF_IN_GA(T512, T514)
QUOTF_IN_GA(s(s(s(s(T564)))), s(T566)) → U14_GA(T564, T566, quotF_in_ga(T564, T566))
QUOTF_IN_GA(s(s(s(s(T564)))), s(T566)) → QUOTF_IN_GA(T564, T566)
QUOTB_IN_GGA(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_GGA(T575, T577, quotG_in_ga(T575, T577))
QUOTB_IN_GGA(s(s(s(T575))), s(s(s(0))), s(T577)) → QUOTG_IN_GA(T575, T577)
QUOTG_IN_GA(s(s(s(T616))), s(T618)) → U15_GA(T616, T618, quotG_in_ga(T616, T618))
QUOTG_IN_GA(s(s(s(T616))), s(T618)) → QUOTG_IN_GA(T616, T618)
QUOTB_IN_GGA(s(s(T626)), s(s(0)), s(T628)) → U9_GGA(T626, T628, quotH_in_ga(T626, T628))
QUOTB_IN_GGA(s(s(T626)), s(s(0)), s(T628)) → QUOTH_IN_GA(T626, T628)
QUOTH_IN_GA(s(s(T656)), s(T658)) → U16_GA(T656, T658, quotH_in_ga(T656, T658))
QUOTH_IN_GA(s(s(T656)), s(T658)) → QUOTH_IN_GA(T656, T658)
QUOTB_IN_GGA(s(T665), s(0), s(T667)) → U10_GGA(T665, T667, quotI_in_ga(T665, T667))
QUOTB_IN_GGA(s(T665), s(0), s(T667)) → QUOTI_IN_GA(T665, T667)
QUOTI_IN_GA(s(T684), s(T686)) → U17_GA(T684, T686, quotI_in_ga(T684, T686))
QUOTI_IN_GA(s(T684), s(T686)) → QUOTI_IN_GA(T684, T686)
divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotA_in_ggga(0, s(T208), T209, 0) → quotA_out_ggga(0, s(T208), T209, 0)
quotA_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
quotA_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quotC_in_ga(T251, T253))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(0))), 0) → quotC_out_ga(s(s(s(0))), 0)
quotC_in_ga(s(s(s(s(0)))), 0) → quotC_out_ga(s(s(s(s(0)))), 0)
quotC_in_ga(s(s(s(s(s(0))))), 0) → quotC_out_ga(s(s(s(s(s(0))))), 0)
quotC_in_ga(s(s(s(s(s(s(0)))))), 0) → quotC_out_ga(s(s(s(s(s(s(0)))))), 0)
quotC_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_ga(T336, T338, quotC_in_ga(T336, T338))
U11_ga(T336, T338, quotC_out_ga(T336, T338)) → quotC_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U4_gga(T251, T253, quotC_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_gga(T350, T352, quotD_in_ga(T350, T352))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U12_ga(T424, T426, quotD_in_ga(T424, T426))
U12_ga(T424, T426, quotD_out_ga(T424, T426)) → quotD_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U5_gga(T350, T352, quotD_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_gga(T437, T439, quotE_in_ga(T437, T439))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T500))))), s(T502)) → U13_ga(T500, T502, quotE_in_ga(T500, T502))
U13_ga(T500, T502, quotE_out_ga(T500, T502)) → quotE_out_ga(s(s(s(s(s(T500))))), s(T502))
U6_gga(T437, T439, quotE_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_gga(T512, T514, quotF_in_ga(T512, T514))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(T564)))), s(T566)) → U14_ga(T564, T566, quotF_in_ga(T564, T566))
U14_ga(T564, T566, quotF_out_ga(T564, T566)) → quotF_out_ga(s(s(s(s(T564)))), s(T566))
U7_gga(T512, T514, quotF_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_gga(T575, T577, quotG_in_ga(T575, T577))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(T616))), s(T618)) → U15_ga(T616, T618, quotG_in_ga(T616, T618))
U15_ga(T616, T618, quotG_out_ga(T616, T618)) → quotG_out_ga(s(s(s(T616))), s(T618))
U8_gga(T575, T577, quotG_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U9_gga(T626, T628, quotH_in_ga(T626, T628))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(T656)), s(T658)) → U16_ga(T656, T658, quotH_in_ga(T656, T658))
U16_ga(T656, T658, quotH_out_ga(T656, T658)) → quotH_out_ga(s(s(T656)), s(T658))
U9_gga(T626, T628, quotH_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U10_gga(T665, T667, quotI_in_ga(T665, T667))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(T684), s(T686)) → U17_ga(T684, T686, quotI_in_ga(T684, T686))
U17_ga(T684, T686, quotI_out_ga(T684, T686)) → quotI_out_ga(s(T684), s(T686))
U10_gga(T665, T667, quotI_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U2_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotA_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quotA_out_ggga(T226, T227, T228, T230)) → quotA_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quotA_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)
DIVJ_IN_GGA(T7, T8, T10) → U18_GGA(T7, T8, T10, quotB_in_gga(T7, T8, T10))
DIVJ_IN_GGA(T7, T8, T10) → QUOTB_IN_GGA(T7, T8, T10)
QUOTB_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_GGA(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
QUOTB_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → QUOTA_IN_GGGA(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)
QUOTA_IN_GGGA(s(T226), s(T227), T228, T230) → U1_GGGA(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
QUOTA_IN_GGGA(s(T226), s(T227), T228, T230) → QUOTA_IN_GGGA(T226, T227, T228, T230)
QUOTA_IN_GGGA(T241, 0, T242, s(T244)) → U2_GGGA(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
QUOTA_IN_GGGA(T241, 0, T242, s(T244)) → QUOTB_IN_GGA(T241, s(T242), T244)
QUOTB_IN_GGA(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_GGA(T251, T253, quotC_in_ga(T251, T253))
QUOTB_IN_GGA(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → QUOTC_IN_GA(T251, T253)
QUOTC_IN_GA(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_GA(T336, T338, quotC_in_ga(T336, T338))
QUOTC_IN_GA(s(s(s(s(s(s(s(T336))))))), s(T338)) → QUOTC_IN_GA(T336, T338)
QUOTB_IN_GGA(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_GGA(T350, T352, quotD_in_ga(T350, T352))
QUOTB_IN_GGA(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → QUOTD_IN_GA(T350, T352)
QUOTD_IN_GA(s(s(s(s(s(s(T424)))))), s(T426)) → U12_GA(T424, T426, quotD_in_ga(T424, T426))
QUOTD_IN_GA(s(s(s(s(s(s(T424)))))), s(T426)) → QUOTD_IN_GA(T424, T426)
QUOTB_IN_GGA(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_GGA(T437, T439, quotE_in_ga(T437, T439))
QUOTB_IN_GGA(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → QUOTE_IN_GA(T437, T439)
QUOTE_IN_GA(s(s(s(s(s(T500))))), s(T502)) → U13_GA(T500, T502, quotE_in_ga(T500, T502))
QUOTE_IN_GA(s(s(s(s(s(T500))))), s(T502)) → QUOTE_IN_GA(T500, T502)
QUOTB_IN_GGA(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_GGA(T512, T514, quotF_in_ga(T512, T514))
QUOTB_IN_GGA(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → QUOTF_IN_GA(T512, T514)
QUOTF_IN_GA(s(s(s(s(T564)))), s(T566)) → U14_GA(T564, T566, quotF_in_ga(T564, T566))
QUOTF_IN_GA(s(s(s(s(T564)))), s(T566)) → QUOTF_IN_GA(T564, T566)
QUOTB_IN_GGA(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_GGA(T575, T577, quotG_in_ga(T575, T577))
QUOTB_IN_GGA(s(s(s(T575))), s(s(s(0))), s(T577)) → QUOTG_IN_GA(T575, T577)
QUOTG_IN_GA(s(s(s(T616))), s(T618)) → U15_GA(T616, T618, quotG_in_ga(T616, T618))
QUOTG_IN_GA(s(s(s(T616))), s(T618)) → QUOTG_IN_GA(T616, T618)
QUOTB_IN_GGA(s(s(T626)), s(s(0)), s(T628)) → U9_GGA(T626, T628, quotH_in_ga(T626, T628))
QUOTB_IN_GGA(s(s(T626)), s(s(0)), s(T628)) → QUOTH_IN_GA(T626, T628)
QUOTH_IN_GA(s(s(T656)), s(T658)) → U16_GA(T656, T658, quotH_in_ga(T656, T658))
QUOTH_IN_GA(s(s(T656)), s(T658)) → QUOTH_IN_GA(T656, T658)
QUOTB_IN_GGA(s(T665), s(0), s(T667)) → U10_GGA(T665, T667, quotI_in_ga(T665, T667))
QUOTB_IN_GGA(s(T665), s(0), s(T667)) → QUOTI_IN_GA(T665, T667)
QUOTI_IN_GA(s(T684), s(T686)) → U17_GA(T684, T686, quotI_in_ga(T684, T686))
QUOTI_IN_GA(s(T684), s(T686)) → QUOTI_IN_GA(T684, T686)
divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotA_in_ggga(0, s(T208), T209, 0) → quotA_out_ggga(0, s(T208), T209, 0)
quotA_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
quotA_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quotC_in_ga(T251, T253))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(0))), 0) → quotC_out_ga(s(s(s(0))), 0)
quotC_in_ga(s(s(s(s(0)))), 0) → quotC_out_ga(s(s(s(s(0)))), 0)
quotC_in_ga(s(s(s(s(s(0))))), 0) → quotC_out_ga(s(s(s(s(s(0))))), 0)
quotC_in_ga(s(s(s(s(s(s(0)))))), 0) → quotC_out_ga(s(s(s(s(s(s(0)))))), 0)
quotC_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_ga(T336, T338, quotC_in_ga(T336, T338))
U11_ga(T336, T338, quotC_out_ga(T336, T338)) → quotC_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U4_gga(T251, T253, quotC_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_gga(T350, T352, quotD_in_ga(T350, T352))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U12_ga(T424, T426, quotD_in_ga(T424, T426))
U12_ga(T424, T426, quotD_out_ga(T424, T426)) → quotD_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U5_gga(T350, T352, quotD_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_gga(T437, T439, quotE_in_ga(T437, T439))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T500))))), s(T502)) → U13_ga(T500, T502, quotE_in_ga(T500, T502))
U13_ga(T500, T502, quotE_out_ga(T500, T502)) → quotE_out_ga(s(s(s(s(s(T500))))), s(T502))
U6_gga(T437, T439, quotE_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_gga(T512, T514, quotF_in_ga(T512, T514))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(T564)))), s(T566)) → U14_ga(T564, T566, quotF_in_ga(T564, T566))
U14_ga(T564, T566, quotF_out_ga(T564, T566)) → quotF_out_ga(s(s(s(s(T564)))), s(T566))
U7_gga(T512, T514, quotF_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_gga(T575, T577, quotG_in_ga(T575, T577))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(T616))), s(T618)) → U15_ga(T616, T618, quotG_in_ga(T616, T618))
U15_ga(T616, T618, quotG_out_ga(T616, T618)) → quotG_out_ga(s(s(s(T616))), s(T618))
U8_gga(T575, T577, quotG_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U9_gga(T626, T628, quotH_in_ga(T626, T628))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(T656)), s(T658)) → U16_ga(T656, T658, quotH_in_ga(T656, T658))
U16_ga(T656, T658, quotH_out_ga(T656, T658)) → quotH_out_ga(s(s(T656)), s(T658))
U9_gga(T626, T628, quotH_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U10_gga(T665, T667, quotI_in_ga(T665, T667))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(T684), s(T686)) → U17_ga(T684, T686, quotI_in_ga(T684, T686))
U17_ga(T684, T686, quotI_out_ga(T684, T686)) → quotI_out_ga(s(T684), s(T686))
U10_gga(T665, T667, quotI_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U2_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotA_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quotA_out_ggga(T226, T227, T228, T230)) → quotA_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quotA_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)
QUOTI_IN_GA(s(T684), s(T686)) → QUOTI_IN_GA(T684, T686)
divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotA_in_ggga(0, s(T208), T209, 0) → quotA_out_ggga(0, s(T208), T209, 0)
quotA_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
quotA_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quotC_in_ga(T251, T253))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(0))), 0) → quotC_out_ga(s(s(s(0))), 0)
quotC_in_ga(s(s(s(s(0)))), 0) → quotC_out_ga(s(s(s(s(0)))), 0)
quotC_in_ga(s(s(s(s(s(0))))), 0) → quotC_out_ga(s(s(s(s(s(0))))), 0)
quotC_in_ga(s(s(s(s(s(s(0)))))), 0) → quotC_out_ga(s(s(s(s(s(s(0)))))), 0)
quotC_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_ga(T336, T338, quotC_in_ga(T336, T338))
U11_ga(T336, T338, quotC_out_ga(T336, T338)) → quotC_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U4_gga(T251, T253, quotC_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_gga(T350, T352, quotD_in_ga(T350, T352))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U12_ga(T424, T426, quotD_in_ga(T424, T426))
U12_ga(T424, T426, quotD_out_ga(T424, T426)) → quotD_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U5_gga(T350, T352, quotD_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_gga(T437, T439, quotE_in_ga(T437, T439))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T500))))), s(T502)) → U13_ga(T500, T502, quotE_in_ga(T500, T502))
U13_ga(T500, T502, quotE_out_ga(T500, T502)) → quotE_out_ga(s(s(s(s(s(T500))))), s(T502))
U6_gga(T437, T439, quotE_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_gga(T512, T514, quotF_in_ga(T512, T514))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(T564)))), s(T566)) → U14_ga(T564, T566, quotF_in_ga(T564, T566))
U14_ga(T564, T566, quotF_out_ga(T564, T566)) → quotF_out_ga(s(s(s(s(T564)))), s(T566))
U7_gga(T512, T514, quotF_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_gga(T575, T577, quotG_in_ga(T575, T577))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(T616))), s(T618)) → U15_ga(T616, T618, quotG_in_ga(T616, T618))
U15_ga(T616, T618, quotG_out_ga(T616, T618)) → quotG_out_ga(s(s(s(T616))), s(T618))
U8_gga(T575, T577, quotG_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U9_gga(T626, T628, quotH_in_ga(T626, T628))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(T656)), s(T658)) → U16_ga(T656, T658, quotH_in_ga(T656, T658))
U16_ga(T656, T658, quotH_out_ga(T656, T658)) → quotH_out_ga(s(s(T656)), s(T658))
U9_gga(T626, T628, quotH_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U10_gga(T665, T667, quotI_in_ga(T665, T667))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(T684), s(T686)) → U17_ga(T684, T686, quotI_in_ga(T684, T686))
U17_ga(T684, T686, quotI_out_ga(T684, T686)) → quotI_out_ga(s(T684), s(T686))
U10_gga(T665, T667, quotI_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U2_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotA_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quotA_out_ggga(T226, T227, T228, T230)) → quotA_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quotA_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)
QUOTI_IN_GA(s(T684), s(T686)) → QUOTI_IN_GA(T684, T686)
QUOTI_IN_GA(s(T684)) → QUOTI_IN_GA(T684)
From the DPs we obtained the following set of size-change graphs:
QUOTH_IN_GA(s(s(T656)), s(T658)) → QUOTH_IN_GA(T656, T658)
divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotA_in_ggga(0, s(T208), T209, 0) → quotA_out_ggga(0, s(T208), T209, 0)
quotA_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
quotA_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quotC_in_ga(T251, T253))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(0))), 0) → quotC_out_ga(s(s(s(0))), 0)
quotC_in_ga(s(s(s(s(0)))), 0) → quotC_out_ga(s(s(s(s(0)))), 0)
quotC_in_ga(s(s(s(s(s(0))))), 0) → quotC_out_ga(s(s(s(s(s(0))))), 0)
quotC_in_ga(s(s(s(s(s(s(0)))))), 0) → quotC_out_ga(s(s(s(s(s(s(0)))))), 0)
quotC_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_ga(T336, T338, quotC_in_ga(T336, T338))
U11_ga(T336, T338, quotC_out_ga(T336, T338)) → quotC_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U4_gga(T251, T253, quotC_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_gga(T350, T352, quotD_in_ga(T350, T352))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U12_ga(T424, T426, quotD_in_ga(T424, T426))
U12_ga(T424, T426, quotD_out_ga(T424, T426)) → quotD_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U5_gga(T350, T352, quotD_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_gga(T437, T439, quotE_in_ga(T437, T439))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T500))))), s(T502)) → U13_ga(T500, T502, quotE_in_ga(T500, T502))
U13_ga(T500, T502, quotE_out_ga(T500, T502)) → quotE_out_ga(s(s(s(s(s(T500))))), s(T502))
U6_gga(T437, T439, quotE_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_gga(T512, T514, quotF_in_ga(T512, T514))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(T564)))), s(T566)) → U14_ga(T564, T566, quotF_in_ga(T564, T566))
U14_ga(T564, T566, quotF_out_ga(T564, T566)) → quotF_out_ga(s(s(s(s(T564)))), s(T566))
U7_gga(T512, T514, quotF_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_gga(T575, T577, quotG_in_ga(T575, T577))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(T616))), s(T618)) → U15_ga(T616, T618, quotG_in_ga(T616, T618))
U15_ga(T616, T618, quotG_out_ga(T616, T618)) → quotG_out_ga(s(s(s(T616))), s(T618))
U8_gga(T575, T577, quotG_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U9_gga(T626, T628, quotH_in_ga(T626, T628))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(T656)), s(T658)) → U16_ga(T656, T658, quotH_in_ga(T656, T658))
U16_ga(T656, T658, quotH_out_ga(T656, T658)) → quotH_out_ga(s(s(T656)), s(T658))
U9_gga(T626, T628, quotH_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U10_gga(T665, T667, quotI_in_ga(T665, T667))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(T684), s(T686)) → U17_ga(T684, T686, quotI_in_ga(T684, T686))
U17_ga(T684, T686, quotI_out_ga(T684, T686)) → quotI_out_ga(s(T684), s(T686))
U10_gga(T665, T667, quotI_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U2_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotA_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quotA_out_ggga(T226, T227, T228, T230)) → quotA_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quotA_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)
QUOTH_IN_GA(s(s(T656)), s(T658)) → QUOTH_IN_GA(T656, T658)
QUOTH_IN_GA(s(s(T656))) → QUOTH_IN_GA(T656)
From the DPs we obtained the following set of size-change graphs:
QUOTG_IN_GA(s(s(s(T616))), s(T618)) → QUOTG_IN_GA(T616, T618)
divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotA_in_ggga(0, s(T208), T209, 0) → quotA_out_ggga(0, s(T208), T209, 0)
quotA_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
quotA_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quotC_in_ga(T251, T253))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(0))), 0) → quotC_out_ga(s(s(s(0))), 0)
quotC_in_ga(s(s(s(s(0)))), 0) → quotC_out_ga(s(s(s(s(0)))), 0)
quotC_in_ga(s(s(s(s(s(0))))), 0) → quotC_out_ga(s(s(s(s(s(0))))), 0)
quotC_in_ga(s(s(s(s(s(s(0)))))), 0) → quotC_out_ga(s(s(s(s(s(s(0)))))), 0)
quotC_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_ga(T336, T338, quotC_in_ga(T336, T338))
U11_ga(T336, T338, quotC_out_ga(T336, T338)) → quotC_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U4_gga(T251, T253, quotC_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_gga(T350, T352, quotD_in_ga(T350, T352))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U12_ga(T424, T426, quotD_in_ga(T424, T426))
U12_ga(T424, T426, quotD_out_ga(T424, T426)) → quotD_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U5_gga(T350, T352, quotD_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_gga(T437, T439, quotE_in_ga(T437, T439))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T500))))), s(T502)) → U13_ga(T500, T502, quotE_in_ga(T500, T502))
U13_ga(T500, T502, quotE_out_ga(T500, T502)) → quotE_out_ga(s(s(s(s(s(T500))))), s(T502))
U6_gga(T437, T439, quotE_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_gga(T512, T514, quotF_in_ga(T512, T514))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(T564)))), s(T566)) → U14_ga(T564, T566, quotF_in_ga(T564, T566))
U14_ga(T564, T566, quotF_out_ga(T564, T566)) → quotF_out_ga(s(s(s(s(T564)))), s(T566))
U7_gga(T512, T514, quotF_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_gga(T575, T577, quotG_in_ga(T575, T577))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(T616))), s(T618)) → U15_ga(T616, T618, quotG_in_ga(T616, T618))
U15_ga(T616, T618, quotG_out_ga(T616, T618)) → quotG_out_ga(s(s(s(T616))), s(T618))
U8_gga(T575, T577, quotG_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U9_gga(T626, T628, quotH_in_ga(T626, T628))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(T656)), s(T658)) → U16_ga(T656, T658, quotH_in_ga(T656, T658))
U16_ga(T656, T658, quotH_out_ga(T656, T658)) → quotH_out_ga(s(s(T656)), s(T658))
U9_gga(T626, T628, quotH_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U10_gga(T665, T667, quotI_in_ga(T665, T667))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(T684), s(T686)) → U17_ga(T684, T686, quotI_in_ga(T684, T686))
U17_ga(T684, T686, quotI_out_ga(T684, T686)) → quotI_out_ga(s(T684), s(T686))
U10_gga(T665, T667, quotI_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U2_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotA_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quotA_out_ggga(T226, T227, T228, T230)) → quotA_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quotA_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)
QUOTG_IN_GA(s(s(s(T616))), s(T618)) → QUOTG_IN_GA(T616, T618)
QUOTG_IN_GA(s(s(s(T616)))) → QUOTG_IN_GA(T616)
From the DPs we obtained the following set of size-change graphs:
QUOTF_IN_GA(s(s(s(s(T564)))), s(T566)) → QUOTF_IN_GA(T564, T566)
divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotA_in_ggga(0, s(T208), T209, 0) → quotA_out_ggga(0, s(T208), T209, 0)
quotA_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
quotA_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quotC_in_ga(T251, T253))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(0))), 0) → quotC_out_ga(s(s(s(0))), 0)
quotC_in_ga(s(s(s(s(0)))), 0) → quotC_out_ga(s(s(s(s(0)))), 0)
quotC_in_ga(s(s(s(s(s(0))))), 0) → quotC_out_ga(s(s(s(s(s(0))))), 0)
quotC_in_ga(s(s(s(s(s(s(0)))))), 0) → quotC_out_ga(s(s(s(s(s(s(0)))))), 0)
quotC_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_ga(T336, T338, quotC_in_ga(T336, T338))
U11_ga(T336, T338, quotC_out_ga(T336, T338)) → quotC_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U4_gga(T251, T253, quotC_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_gga(T350, T352, quotD_in_ga(T350, T352))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U12_ga(T424, T426, quotD_in_ga(T424, T426))
U12_ga(T424, T426, quotD_out_ga(T424, T426)) → quotD_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U5_gga(T350, T352, quotD_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_gga(T437, T439, quotE_in_ga(T437, T439))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T500))))), s(T502)) → U13_ga(T500, T502, quotE_in_ga(T500, T502))
U13_ga(T500, T502, quotE_out_ga(T500, T502)) → quotE_out_ga(s(s(s(s(s(T500))))), s(T502))
U6_gga(T437, T439, quotE_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_gga(T512, T514, quotF_in_ga(T512, T514))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(T564)))), s(T566)) → U14_ga(T564, T566, quotF_in_ga(T564, T566))
U14_ga(T564, T566, quotF_out_ga(T564, T566)) → quotF_out_ga(s(s(s(s(T564)))), s(T566))
U7_gga(T512, T514, quotF_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_gga(T575, T577, quotG_in_ga(T575, T577))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(T616))), s(T618)) → U15_ga(T616, T618, quotG_in_ga(T616, T618))
U15_ga(T616, T618, quotG_out_ga(T616, T618)) → quotG_out_ga(s(s(s(T616))), s(T618))
U8_gga(T575, T577, quotG_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U9_gga(T626, T628, quotH_in_ga(T626, T628))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(T656)), s(T658)) → U16_ga(T656, T658, quotH_in_ga(T656, T658))
U16_ga(T656, T658, quotH_out_ga(T656, T658)) → quotH_out_ga(s(s(T656)), s(T658))
U9_gga(T626, T628, quotH_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U10_gga(T665, T667, quotI_in_ga(T665, T667))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(T684), s(T686)) → U17_ga(T684, T686, quotI_in_ga(T684, T686))
U17_ga(T684, T686, quotI_out_ga(T684, T686)) → quotI_out_ga(s(T684), s(T686))
U10_gga(T665, T667, quotI_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U2_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotA_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quotA_out_ggga(T226, T227, T228, T230)) → quotA_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quotA_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)
QUOTF_IN_GA(s(s(s(s(T564)))), s(T566)) → QUOTF_IN_GA(T564, T566)
QUOTF_IN_GA(s(s(s(s(T564))))) → QUOTF_IN_GA(T564)
From the DPs we obtained the following set of size-change graphs:
QUOTE_IN_GA(s(s(s(s(s(T500))))), s(T502)) → QUOTE_IN_GA(T500, T502)
divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotA_in_ggga(0, s(T208), T209, 0) → quotA_out_ggga(0, s(T208), T209, 0)
quotA_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
quotA_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quotC_in_ga(T251, T253))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(0))), 0) → quotC_out_ga(s(s(s(0))), 0)
quotC_in_ga(s(s(s(s(0)))), 0) → quotC_out_ga(s(s(s(s(0)))), 0)
quotC_in_ga(s(s(s(s(s(0))))), 0) → quotC_out_ga(s(s(s(s(s(0))))), 0)
quotC_in_ga(s(s(s(s(s(s(0)))))), 0) → quotC_out_ga(s(s(s(s(s(s(0)))))), 0)
quotC_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_ga(T336, T338, quotC_in_ga(T336, T338))
U11_ga(T336, T338, quotC_out_ga(T336, T338)) → quotC_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U4_gga(T251, T253, quotC_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_gga(T350, T352, quotD_in_ga(T350, T352))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U12_ga(T424, T426, quotD_in_ga(T424, T426))
U12_ga(T424, T426, quotD_out_ga(T424, T426)) → quotD_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U5_gga(T350, T352, quotD_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_gga(T437, T439, quotE_in_ga(T437, T439))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T500))))), s(T502)) → U13_ga(T500, T502, quotE_in_ga(T500, T502))
U13_ga(T500, T502, quotE_out_ga(T500, T502)) → quotE_out_ga(s(s(s(s(s(T500))))), s(T502))
U6_gga(T437, T439, quotE_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_gga(T512, T514, quotF_in_ga(T512, T514))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(T564)))), s(T566)) → U14_ga(T564, T566, quotF_in_ga(T564, T566))
U14_ga(T564, T566, quotF_out_ga(T564, T566)) → quotF_out_ga(s(s(s(s(T564)))), s(T566))
U7_gga(T512, T514, quotF_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_gga(T575, T577, quotG_in_ga(T575, T577))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(T616))), s(T618)) → U15_ga(T616, T618, quotG_in_ga(T616, T618))
U15_ga(T616, T618, quotG_out_ga(T616, T618)) → quotG_out_ga(s(s(s(T616))), s(T618))
U8_gga(T575, T577, quotG_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U9_gga(T626, T628, quotH_in_ga(T626, T628))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(T656)), s(T658)) → U16_ga(T656, T658, quotH_in_ga(T656, T658))
U16_ga(T656, T658, quotH_out_ga(T656, T658)) → quotH_out_ga(s(s(T656)), s(T658))
U9_gga(T626, T628, quotH_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U10_gga(T665, T667, quotI_in_ga(T665, T667))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(T684), s(T686)) → U17_ga(T684, T686, quotI_in_ga(T684, T686))
U17_ga(T684, T686, quotI_out_ga(T684, T686)) → quotI_out_ga(s(T684), s(T686))
U10_gga(T665, T667, quotI_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U2_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotA_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quotA_out_ggga(T226, T227, T228, T230)) → quotA_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quotA_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)
QUOTE_IN_GA(s(s(s(s(s(T500))))), s(T502)) → QUOTE_IN_GA(T500, T502)
QUOTE_IN_GA(s(s(s(s(s(T500)))))) → QUOTE_IN_GA(T500)
From the DPs we obtained the following set of size-change graphs:
QUOTD_IN_GA(s(s(s(s(s(s(T424)))))), s(T426)) → QUOTD_IN_GA(T424, T426)
divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotA_in_ggga(0, s(T208), T209, 0) → quotA_out_ggga(0, s(T208), T209, 0)
quotA_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
quotA_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quotC_in_ga(T251, T253))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(0))), 0) → quotC_out_ga(s(s(s(0))), 0)
quotC_in_ga(s(s(s(s(0)))), 0) → quotC_out_ga(s(s(s(s(0)))), 0)
quotC_in_ga(s(s(s(s(s(0))))), 0) → quotC_out_ga(s(s(s(s(s(0))))), 0)
quotC_in_ga(s(s(s(s(s(s(0)))))), 0) → quotC_out_ga(s(s(s(s(s(s(0)))))), 0)
quotC_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_ga(T336, T338, quotC_in_ga(T336, T338))
U11_ga(T336, T338, quotC_out_ga(T336, T338)) → quotC_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U4_gga(T251, T253, quotC_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_gga(T350, T352, quotD_in_ga(T350, T352))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U12_ga(T424, T426, quotD_in_ga(T424, T426))
U12_ga(T424, T426, quotD_out_ga(T424, T426)) → quotD_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U5_gga(T350, T352, quotD_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_gga(T437, T439, quotE_in_ga(T437, T439))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T500))))), s(T502)) → U13_ga(T500, T502, quotE_in_ga(T500, T502))
U13_ga(T500, T502, quotE_out_ga(T500, T502)) → quotE_out_ga(s(s(s(s(s(T500))))), s(T502))
U6_gga(T437, T439, quotE_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_gga(T512, T514, quotF_in_ga(T512, T514))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(T564)))), s(T566)) → U14_ga(T564, T566, quotF_in_ga(T564, T566))
U14_ga(T564, T566, quotF_out_ga(T564, T566)) → quotF_out_ga(s(s(s(s(T564)))), s(T566))
U7_gga(T512, T514, quotF_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_gga(T575, T577, quotG_in_ga(T575, T577))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(T616))), s(T618)) → U15_ga(T616, T618, quotG_in_ga(T616, T618))
U15_ga(T616, T618, quotG_out_ga(T616, T618)) → quotG_out_ga(s(s(s(T616))), s(T618))
U8_gga(T575, T577, quotG_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U9_gga(T626, T628, quotH_in_ga(T626, T628))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(T656)), s(T658)) → U16_ga(T656, T658, quotH_in_ga(T656, T658))
U16_ga(T656, T658, quotH_out_ga(T656, T658)) → quotH_out_ga(s(s(T656)), s(T658))
U9_gga(T626, T628, quotH_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U10_gga(T665, T667, quotI_in_ga(T665, T667))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(T684), s(T686)) → U17_ga(T684, T686, quotI_in_ga(T684, T686))
U17_ga(T684, T686, quotI_out_ga(T684, T686)) → quotI_out_ga(s(T684), s(T686))
U10_gga(T665, T667, quotI_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U2_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotA_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quotA_out_ggga(T226, T227, T228, T230)) → quotA_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quotA_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)
QUOTD_IN_GA(s(s(s(s(s(s(T424)))))), s(T426)) → QUOTD_IN_GA(T424, T426)
QUOTD_IN_GA(s(s(s(s(s(s(T424))))))) → QUOTD_IN_GA(T424)
From the DPs we obtained the following set of size-change graphs:
QUOTC_IN_GA(s(s(s(s(s(s(s(T336))))))), s(T338)) → QUOTC_IN_GA(T336, T338)
divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotA_in_ggga(0, s(T208), T209, 0) → quotA_out_ggga(0, s(T208), T209, 0)
quotA_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
quotA_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quotC_in_ga(T251, T253))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(0))), 0) → quotC_out_ga(s(s(s(0))), 0)
quotC_in_ga(s(s(s(s(0)))), 0) → quotC_out_ga(s(s(s(s(0)))), 0)
quotC_in_ga(s(s(s(s(s(0))))), 0) → quotC_out_ga(s(s(s(s(s(0))))), 0)
quotC_in_ga(s(s(s(s(s(s(0)))))), 0) → quotC_out_ga(s(s(s(s(s(s(0)))))), 0)
quotC_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_ga(T336, T338, quotC_in_ga(T336, T338))
U11_ga(T336, T338, quotC_out_ga(T336, T338)) → quotC_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U4_gga(T251, T253, quotC_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_gga(T350, T352, quotD_in_ga(T350, T352))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U12_ga(T424, T426, quotD_in_ga(T424, T426))
U12_ga(T424, T426, quotD_out_ga(T424, T426)) → quotD_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U5_gga(T350, T352, quotD_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_gga(T437, T439, quotE_in_ga(T437, T439))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T500))))), s(T502)) → U13_ga(T500, T502, quotE_in_ga(T500, T502))
U13_ga(T500, T502, quotE_out_ga(T500, T502)) → quotE_out_ga(s(s(s(s(s(T500))))), s(T502))
U6_gga(T437, T439, quotE_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_gga(T512, T514, quotF_in_ga(T512, T514))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(T564)))), s(T566)) → U14_ga(T564, T566, quotF_in_ga(T564, T566))
U14_ga(T564, T566, quotF_out_ga(T564, T566)) → quotF_out_ga(s(s(s(s(T564)))), s(T566))
U7_gga(T512, T514, quotF_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_gga(T575, T577, quotG_in_ga(T575, T577))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(T616))), s(T618)) → U15_ga(T616, T618, quotG_in_ga(T616, T618))
U15_ga(T616, T618, quotG_out_ga(T616, T618)) → quotG_out_ga(s(s(s(T616))), s(T618))
U8_gga(T575, T577, quotG_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U9_gga(T626, T628, quotH_in_ga(T626, T628))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(T656)), s(T658)) → U16_ga(T656, T658, quotH_in_ga(T656, T658))
U16_ga(T656, T658, quotH_out_ga(T656, T658)) → quotH_out_ga(s(s(T656)), s(T658))
U9_gga(T626, T628, quotH_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U10_gga(T665, T667, quotI_in_ga(T665, T667))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(T684), s(T686)) → U17_ga(T684, T686, quotI_in_ga(T684, T686))
U17_ga(T684, T686, quotI_out_ga(T684, T686)) → quotI_out_ga(s(T684), s(T686))
U10_gga(T665, T667, quotI_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U2_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotA_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quotA_out_ggga(T226, T227, T228, T230)) → quotA_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quotA_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)
QUOTC_IN_GA(s(s(s(s(s(s(s(T336))))))), s(T338)) → QUOTC_IN_GA(T336, T338)
QUOTC_IN_GA(s(s(s(s(s(s(s(T336)))))))) → QUOTC_IN_GA(T336)
From the DPs we obtained the following set of size-change graphs:
QUOTB_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → QUOTA_IN_GGGA(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)
QUOTA_IN_GGGA(s(T226), s(T227), T228, T230) → QUOTA_IN_GGGA(T226, T227, T228, T230)
QUOTA_IN_GGGA(T241, 0, T242, s(T244)) → QUOTB_IN_GGA(T241, s(T242), T244)
divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotB_in_gga(T7, T8, T10))
quotB_in_gga(0, s(T15), 0) → quotB_out_gga(0, s(T15), 0)
quotB_in_gga(s(0), s(s(T38)), 0) → quotB_out_gga(s(0), s(s(T38)), 0)
quotB_in_gga(s(s(0)), s(s(s(T61))), 0) → quotB_out_gga(s(s(0)), s(s(s(T61))), 0)
quotB_in_gga(s(s(s(0))), s(s(s(s(T84)))), 0) → quotB_out_gga(s(s(s(0))), s(s(s(s(T84)))), 0)
quotB_in_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0) → quotB_out_gga(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0)
quotB_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0) → quotB_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0)
quotB_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0) → quotB_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0) → quotB_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0)
quotB_in_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_gga(T189, T190, T192, quotA_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
quotA_in_ggga(0, s(T208), T209, 0) → quotA_out_ggga(0, s(T208), T209, 0)
quotA_in_ggga(s(T226), s(T227), T228, T230) → U1_ggga(T226, T227, T228, T230, quotA_in_ggga(T226, T227, T228, T230))
quotA_in_ggga(T241, 0, T242, s(T244)) → U2_ggga(T241, T242, T244, quotB_in_gga(T241, s(T242), T244))
quotB_in_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_gga(T251, T253, quotC_in_ga(T251, T253))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(0))), 0) → quotC_out_ga(s(s(s(0))), 0)
quotC_in_ga(s(s(s(s(0)))), 0) → quotC_out_ga(s(s(s(s(0)))), 0)
quotC_in_ga(s(s(s(s(s(0))))), 0) → quotC_out_ga(s(s(s(s(s(0))))), 0)
quotC_in_ga(s(s(s(s(s(s(0)))))), 0) → quotC_out_ga(s(s(s(s(s(s(0)))))), 0)
quotC_in_ga(s(s(s(s(s(s(s(T336))))))), s(T338)) → U11_ga(T336, T338, quotC_in_ga(T336, T338))
U11_ga(T336, T338, quotC_out_ga(T336, T338)) → quotC_out_ga(s(s(s(s(s(s(s(T336))))))), s(T338))
U4_gga(T251, T253, quotC_out_ga(T251, T253)) → quotB_out_gga(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253))
quotB_in_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352)) → U5_gga(T350, T352, quotD_in_ga(T350, T352))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(0)))), 0) → quotD_out_ga(s(s(s(s(0)))), 0)
quotD_in_ga(s(s(s(s(s(0))))), 0) → quotD_out_ga(s(s(s(s(s(0))))), 0)
quotD_in_ga(s(s(s(s(s(s(T424)))))), s(T426)) → U12_ga(T424, T426, quotD_in_ga(T424, T426))
U12_ga(T424, T426, quotD_out_ga(T424, T426)) → quotD_out_ga(s(s(s(s(s(s(T424)))))), s(T426))
U5_gga(T350, T352, quotD_out_ga(T350, T352)) → quotB_out_gga(s(s(s(s(s(s(T350)))))), s(s(s(s(s(s(0)))))), s(T352))
quotB_in_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439)) → U6_gga(T437, T439, quotE_in_ga(T437, T439))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T500))))), s(T502)) → U13_ga(T500, T502, quotE_in_ga(T500, T502))
U13_ga(T500, T502, quotE_out_ga(T500, T502)) → quotE_out_ga(s(s(s(s(s(T500))))), s(T502))
U6_gga(T437, T439, quotE_out_ga(T437, T439)) → quotB_out_gga(s(s(s(s(s(T437))))), s(s(s(s(s(0))))), s(T439))
quotB_in_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514)) → U7_gga(T512, T514, quotF_in_ga(T512, T514))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(T564)))), s(T566)) → U14_ga(T564, T566, quotF_in_ga(T564, T566))
U14_ga(T564, T566, quotF_out_ga(T564, T566)) → quotF_out_ga(s(s(s(s(T564)))), s(T566))
U7_gga(T512, T514, quotF_out_ga(T512, T514)) → quotB_out_gga(s(s(s(s(T512)))), s(s(s(s(0)))), s(T514))
quotB_in_gga(s(s(s(T575))), s(s(s(0))), s(T577)) → U8_gga(T575, T577, quotG_in_ga(T575, T577))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(T616))), s(T618)) → U15_ga(T616, T618, quotG_in_ga(T616, T618))
U15_ga(T616, T618, quotG_out_ga(T616, T618)) → quotG_out_ga(s(s(s(T616))), s(T618))
U8_gga(T575, T577, quotG_out_ga(T575, T577)) → quotB_out_gga(s(s(s(T575))), s(s(s(0))), s(T577))
quotB_in_gga(s(s(T626)), s(s(0)), s(T628)) → U9_gga(T626, T628, quotH_in_ga(T626, T628))
quotH_in_ga(0, 0) → quotH_out_ga(0, 0)
quotH_in_ga(s(0), 0) → quotH_out_ga(s(0), 0)
quotH_in_ga(s(s(T656)), s(T658)) → U16_ga(T656, T658, quotH_in_ga(T656, T658))
U16_ga(T656, T658, quotH_out_ga(T656, T658)) → quotH_out_ga(s(s(T656)), s(T658))
U9_gga(T626, T628, quotH_out_ga(T626, T628)) → quotB_out_gga(s(s(T626)), s(s(0)), s(T628))
quotB_in_gga(s(T665), s(0), s(T667)) → U10_gga(T665, T667, quotI_in_ga(T665, T667))
quotI_in_ga(0, 0) → quotI_out_ga(0, 0)
quotI_in_ga(s(T684), s(T686)) → U17_ga(T684, T686, quotI_in_ga(T684, T686))
U17_ga(T684, T686, quotI_out_ga(T684, T686)) → quotI_out_ga(s(T684), s(T686))
U10_gga(T665, T667, quotI_out_ga(T665, T667)) → quotB_out_gga(s(T665), s(0), s(T667))
U2_ggga(T241, T242, T244, quotB_out_gga(T241, s(T242), T244)) → quotA_out_ggga(T241, 0, T242, s(T244))
U1_ggga(T226, T227, T228, T230, quotA_out_ggga(T226, T227, T228, T230)) → quotA_out_ggga(s(T226), s(T227), T228, T230)
U3_gga(T189, T190, T192, quotA_out_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)) → quotB_out_gga(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192)
U18_gga(T7, T8, T10, quotB_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)
QUOTB_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → QUOTA_IN_GGGA(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)
QUOTA_IN_GGGA(s(T226), s(T227), T228, T230) → QUOTA_IN_GGGA(T226, T227, T228, T230)
QUOTA_IN_GGGA(T241, 0, T242, s(T244)) → QUOTB_IN_GGA(T241, s(T242), T244)
QUOTB_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190))))))))) → QUOTA_IN_GGGA(T189, T190, s(s(s(s(s(s(s(T190))))))))
QUOTA_IN_GGGA(s(T226), s(T227), T228) → QUOTA_IN_GGGA(T226, T227, T228)
QUOTA_IN_GGGA(T241, 0, T242) → QUOTB_IN_GGA(T241, s(T242))
From the DPs we obtained the following set of size-change graphs: